COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	unprov[f81,jmc]		Proving unprovability
C00005 ENDMK
C⊗;
unprov[f81,jmc]		Proving unprovability

	It is supposed that the arguments as to why proving unprovability
is important for AI treatments of non-knowledge are understood or
accepted temporarily.  They will be found elsewhere or supplied orally
upon request.

	Suppose we have a sentence  P{m,n,f} of first order logic,
where the braces
indicate that  m  and  n  occur as free individual variables in  P, and
f  occurs as a free function variable.  We assume that  P  is all
a person  S  has been told about a certain subject.  For example, it may
be all that the king has told the wisemen relevant to the colors of
their spots or all that Mr. S and Mr. P have been told about the
numbers  m  and  n.

	We would like to show that on the basis of this information,
S  cannot know the value of some term, say  g(m,n).  Actually, we will
often want to say more.  Namely, we may want to say that  S  doesn't
know that  g(m,n) ≠ 2 and he doesn't know  g(m,n) ≠ 4.  In fact, we
may want to show that given any even number  k,  S doesn't know
g(m,n) ≠ k.

	We propose to do this as follows.  Suppose we can find values
m0, n0 and f0 for m, n and  f respectively, such that  P(m0,n0,f0) is true,
and  g(m0,n0) = 2.  Then if there were a proof that  g(m,n) ≠ 2, the
same proof would show that  2 = g(m0,n0) ≠ 2, which would be
a contradiction.  In the more general case, we would have to find
functions m0(k), n0(k), f0(k) and prove the formula

	∀k.even(k) ⊃ P(m0(k),n0(k),f0(k)) ∧ g(m0(k),n0(k)) = k.

	Thus we would have to parametrize our space of possibilities
with  k  as a parameter.

	Aha, the general result seems to be the following.  Suppose certain
entities x  occur free in our premisses expressed as a sentence P{x}, and
we want to show that for all  y, a sentence  Q{x,y}  is possible.  Then
we only need to prove

	∀y.∃x.P{x}∧Q{x,y}.